(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UFIDL)
(declare-fun v0 () Int)
(declare-fun v1 () Int)
(declare-fun f0 ( Int Int) Int)
(declare-fun f1 ( Int Int Int) Int)
(declare-fun p0 ( Int) Bool)
(assert (let ((e2 6))
(let ((e3 2))
(let ((e4 0))
(let ((e5 (distinct v1 v0)))
(let ((e6 (= (- v0 v1) (- e3))))
(let ((e7 (< v0 v0)))
(let ((e8 (distinct v0 v0)))
(let ((e9 (= (- v0 v1) e3)))
(let ((e10 (> (- v0 v1) (- e2))))
(let ((e11 (= v1 v1)))
(let ((e12 (> v0 v0)))
(let ((e13 (distinct (- v1 v1) (- e3))))
(let ((e14 (> v0 v1)))
(let ((e15 (<= (- v0 v1) e3)))
(let ((e16 (< v0 v1)))
(let ((e17 (<= (- v0 v0) (- e2))))
(let ((e18 (distinct (- v0 v1) (- e2))))
(let ((e19 (distinct v0 v0)))
(let ((e20 (>= (- v0 v0) (- e3))))
(let ((e21 (< (- v1 v1) e2)))
(let ((e22 (<= v0 v0)))
(let ((e23 (< (- v1 v1) e2)))
(let ((e24 (f0 v0 v0)))
(let ((e25 (f1 e24 v0 v1)))
(let ((e26 (f0 v1 v1)))
(let ((e27 (f1 v1 e25 e25)))
(let ((e28 (f0 v1 v1)))
(let ((e29 (f0 e28 e28)))
(let ((e30 (f1 v0 e27 e29)))
(let ((e31 (f1 v0 v0 v0)))
(let ((e32 (= e25 v0)))
(let ((e33 (distinct v1 e24)))
(let ((e34 (p0 e28)))
(let ((e35 (p0 v1)))
(let ((e36 (p0 v1)))
(let ((e37 (p0 e25)))
(let ((e38 (p0 e29)))
(let ((e39 (p0 e26)))
(let ((e40 (p0 e31)))
(let ((e41 (distinct v1 e25)))
(let ((e42 (p0 e24)))
(let ((e43 (= e30 e29)))
(let ((e44 (p0 e24)))
(let ((e45 (p0 e31)))
(let ((e46 (p0 v1)))
(let ((e47 (p0 e27)))
(let ((e48 (distinct e27 e28)))
(let ((e49 (distinct e30 e26)))
(let ((e50 (p0 e29)))
(let ((e51 (p0 e31)))
(let ((e52 (= e26 e31)))
(let ((e53 (p0 v0)))
(let ((e54 (distinct e28 e30)))
(let ((e55 (p0 v0)))
(let ((e56 (p0 v0)))
(let ((e57 (= e29 e25)))
(let ((e58 (p0 v0)))
(let ((e59 (p0 e30)))
(let ((e60 (distinct e27 e30)))
(let ((e61 (p0 e28)))
(let ((e62 (p0 e24)))
(let ((e63 (p0 e27)))
(let ((e64 (p0 v0)))
(let ((e65 (p0 e31)))
(let ((e66 (p0 e28)))
(let ((e67 (p0 e26)))
(let ((e68 (distinct e24 e26)))
(let ((e69 (p0 v1)))
(let ((e70 (= e25 e30)))
(let ((e71 (= e27 e30)))
(let ((e72 (p0 e30)))
(let ((e73 (= e29 e30)))
(let ((e74 (= e28 e28)))
(let ((e75 (< e30 v0)))
(let ((e76 (> e24 e25)))
(let ((e77 (p0 v0)))
(let ((e78 (>= e31 e25)))
(let ((e79 (p0 e26)))
(let ((e80 (p0 e26)))
(let ((e81 (distinct v0 e28)))
(let ((e82 (>= e24 e31)))
(let ((e83 (distinct v0 v1)))
(let ((e84 (< v1 e28)))
(let ((e85 (distinct e28 e27)))
(let ((e86 (= e24 e24)))
(let ((e87 (= e30 e30)))
(let ((e88 (distinct e27 e24)))
(let ((e89 (= e29 e30)))
(let ((e90 (< v1 e26)))
(let ((e91 (> e25 v1)))
(let ((e92 (= v0 e29)))
(let ((e93 (<= e25 e31)))
(let ((e94 (distinct e31 v1)))
(let ((e95 (>= e27 e24)))
(let ((e96 (p0 v1)))
(let ((e97 (> e27 e30)))
(let ((e98 (< e30 e28)))
(let ((e99 (p0 e25)))
(let ((e100 (>= e24 v0)))
(let ((e101 (= e27 e29)))
(let ((e102 (<= e26 e29)))
(let ((e103 (= e25 e29)))
(let ((e104 (> e31 e26)))
(let ((e105 (not e18)))
(let ((e106 (=> e100 e19)))
(let ((e107 (=> e82 e56)))
(let ((e108 (and e50 e35)))
(let ((e109 (not e63)))
(let ((e110 (or e49 e7)))
(let ((e111 (ite e84 e74 e86)))
(let ((e112 (ite e43 e97 e16)))
(let ((e113 (ite e99 e54 e46)))
(let ((e114 (or e85 e106)))
(let ((e115 (not e36)))
(let ((e116 (or e75 e93)))
(let ((e117 (ite e67 e6 e71)))
(let ((e118 (= e73 e89)))
(let ((e119 (= e34 e51)))
(let ((e120 (= e92 e68)))
(let ((e121 (ite e41 e109 e116)))
(let ((e122 (= e22 e96)))
(let ((e123 (ite e60 e108 e121)))
(let ((e124 (= e44 e39)))
(let ((e125 (= e45 e105)))
(let ((e126 (and e42 e15)))
(let ((e127 (and e87 e5)))
(let ((e128 (=> e83 e101)))
(let ((e129 (=> e65 e21)))
(let ((e130 (=> e13 e52)))
(let ((e131 (xor e62 e10)))
(let ((e132 (=> e126 e23)))
(let ((e133 (xor e40 e124)))
(let ((e134 (=> e115 e32)))
(let ((e135 (ite e58 e114 e20)))
(let ((e136 (and e11 e8)))
(let ((e137 (or e119 e123)))
(let ((e138 (xor e79 e57)))
(let ((e139 (xor e122 e125)))
(let ((e140 (ite e135 e95 e48)))
(let ((e141 (=> e137 e140)))
(let ((e142 (=> e133 e64)))
(let ((e143 (=> e130 e138)))
(let ((e144 (= e107 e9)))
(let ((e145 (or e53 e129)))
(let ((e146 (= e12 e33)))
(let ((e147 (xor e111 e66)))
(let ((e148 (and e141 e59)))
(let ((e149 (not e72)))
(let ((e150 (ite e127 e142 e98)))
(let ((e151 (xor e61 e47)))
(let ((e152 (and e120 e136)))
(let ((e153 (=> e70 e91)))
(let ((e154 (ite e148 e17 e143)))
(let ((e155 (=> e152 e144)))
(let ((e156 (not e14)))
(let ((e157 (ite e104 e88 e151)))
(let ((e158 (or e112 e131)))
(let ((e159 (not e55)))
(let ((e160 (ite e158 e38 e76)))
(let ((e161 (not e139)))
(let ((e162 (not e155)))
(let ((e163 (not e110)))
(let ((e164 (or e162 e78)))
(let ((e165 (ite e103 e134 e163)))
(let ((e166 (ite e145 e157 e69)))
(let ((e167 (= e117 e161)))
(let ((e168 (=> e118 e118)))
(let ((e169 (ite e146 e77 e146)))
(let ((e170 (or e132 e159)))
(let ((e171 (not e165)))
(let ((e172 (not e156)))
(let ((e173 (= e172 e164)))
(let ((e174 (xor e94 e153)))
(let ((e175 (xor e149 e160)))
(let ((e176 (=> e147 e81)))
(let ((e177 (=> e175 e173)))
(let ((e178 (=> e113 e166)))
(let ((e179 (= e170 e168)))
(let ((e180 (and e90 e167)))
(let ((e181 (not e171)))
(let ((e182 (or e177 e174)))
(let ((e183 (xor e128 e180)))
(let ((e184 (= e183 e183)))
(let ((e185 (and e179 e181)))
(let ((e186 (= e80 e169)))
(let ((e187 (and e102 e154)))
(let ((e188 (ite e150 e37 e184)))
(let ((e189 (or e176 e176)))
(let ((e190 (=> e178 e182)))
(let ((e191 (xor e185 e185)))
(let ((e192 (ite e189 e189 e190)))
(let ((e193 (or e186 e186)))
(let ((e194 (not e192)))
(let ((e195 (and e191 e187)))
(let ((e196 (xor e194 e195)))
(let ((e197 (not e193)))
(let ((e198 (ite e188 e196 e196)))
(let ((e199 (or e198 e198)))
(let ((e200 (and e199 e199)))
(let ((e201 (and e200 e197)))
e201
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
